Inference at * 2 1 
Iof proof for Lemma dcdr-to-bool-equivalence:



1. P : 
2. x : P
3. P
  [inl x ] 

latex

 by (RepUR ``dcdr-to-bool assert`` ( 0)) 
CollapseTHEN (Trivial) 

latex

C.

Definitions

[d], b, True, t  T